\begin{tabbing}
OCMon\{i\}
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\{\=$g$:AbMon\{i\}$\mid$ \+
\\[0ex]Linorder($\mid$$g$$\mid$;$x$,$y$.$\uparrow$($x$ ($\leq_{b}$$g$) $y$))
\\[0ex]\& Cancel($\mid$$g$$\mid$;$\mid$$g$$\mid$;$\ast$$g$)
\\[0ex]\& ($\forall$$z$:$\mid$$g$$\mid$. monot($\mid$$g$$\mid$;$x$,$y$.$\uparrow$($x$ ($\leq_{b}$$g$) $y$);$\lambda$$w$.$z$ ($\ast$$g$) $w$))\} 
\-
\end{tabbing}